This PR adds the core components for a backend-independent counterexample model, to be used in either backend using the command line parameter --counterexample=extended.
Unlike the current --counterexample=variables option, it contains information not just about local variables, but also about the heap, functions, etc.
Unlike Silicon's current --counterexample=mapped, which is exclusive to Silicon, the new model also supports quantified permissions and wands, and also works in Carbon.

Implementations in Silicon and Carbon will get their own PRs.

This is the result of @rvandoren's practical work project, with a bunch of additions from me.